\subsection{\auto\ XML file format}

Here is an example of an XML file representing an \auto\:
\lstset{language=XML,
		basicstyle=\scriptsize\ttfamily
	    , emph={state,automaton,states,transitions, transition}
    	, emphstyle=\color{red}
    	, emph={[2]id, stateName, name, initial, final, origin, target, label}
	    , emphstyle={[2]\color{green}}}

\begin{center}
\begin{lstlisting}[frame=single, caption={Example of an \auto\ in XML}, label=example1] 

<automaton name="example">]
	<states>
		<state id="1" stateName="E1" initial="true" final="false"/>
		<state id="2" stateName="E2" initial="false" final="false"/>
		<state id="3" stateName="E3" initial="false" final="false"/>
		<state id="4" stateName="E4" initial="false" final="true"/>
	</states>
	<transitions>
		<transition origin="1" target="2" label="a"/>
		<transition origin="2" target="3" label="a"/>
		<transition origin="3" target="4" label="a"/>
		<transition origin="1" target="1" label="b"/>
		<transition origin="1" target="4" label="b"/>
	</transitions>
</automaton>

\end{lstlisting}
\end{center}

As you can see in listing \ref{example1}, it is quite simple and easy to read. The file is separated in two parts, first the definition of the \st s and then the \tr s between those \st s.\mk

A \st\ is defined by a unique identifier which simply is a number, then come its name and whether it is an initial or final \st . Any \auto\ might posses several initial states as well as finals.\mk

A \tr\ is composed of two \st s' references one for its origin, and the other for the targeted one. And of course the last element is the transition's label.\bk
